0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxTypedWeightedTrs
↳7 CompletionProof (UPPER BOUND(ID), 0 ms)
↳8 CpxTypedWeightedCompleteTrs
↳9 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳10 CpxRNTS
↳11 CompleteCoflocoProof (⇔, 1382 ms)
↳12 BOUNDS(1, n^2)
p(s(N)) → N
+(N, 0) → N
+(s(N), s(M)) → s(s(+(N, M)))
*(N, 0) → 0
*(s(N), s(M)) → s(+(N, +(M, *(N, M))))
gt(0, M) → False
gt(NzN, 0) → u_4(is_NzNat(NzN))
u_4(True) → True
is_NzNat(0) → False
is_NzNat(s(N)) → True
gt(s(N), s(M)) → gt(N, M)
lt(N, M) → gt(M, N)
d(0, N) → N
d(s(N), s(M)) → d(N, M)
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM)
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM)
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM))
quot(NzM, NzM) → u_01(is_NzNat(NzM))
u_01(True) → s(0)
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N)
u_21(True, NzM, N) → u_2(gt(NzM, N))
u_2(True) → 0
gcd(0, N) → 0
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM)
u_02(True, NzM) → NzM
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM)
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM)
p(s(N)) → N [1]
+(N, 0) → N [1]
+(s(N), s(M)) → s(s(+(N, M))) [1]
*(N, 0) → 0 [1]
*(s(N), s(M)) → s(+(N, +(M, *(N, M)))) [1]
gt(0, M) → False [1]
gt(NzN, 0) → u_4(is_NzNat(NzN)) [1]
u_4(True) → True [1]
is_NzNat(0) → False [1]
is_NzNat(s(N)) → True [1]
gt(s(N), s(M)) → gt(N, M) [1]
lt(N, M) → gt(M, N) [1]
d(0, N) → N [1]
d(s(N), s(M)) → d(N, M) [1]
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM) [1]
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM) [1]
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM)) [1]
quot(NzM, NzM) → u_01(is_NzNat(NzM)) [1]
u_01(True) → s(0) [1]
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N) [1]
u_21(True, NzM, N) → u_2(gt(NzM, N)) [1]
u_2(True) → 0 [1]
gcd(0, N) → 0 [1]
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM) [1]
u_02(True, NzM) → NzM [1]
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) [1]
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM) [1]
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM) [1]
| + => plus |
| * => times |
p(s(N)) → N [1]
plus(N, 0) → N [1]
plus(s(N), s(M)) → s(s(plus(N, M))) [1]
times(N, 0) → 0 [1]
times(s(N), s(M)) → s(plus(N, plus(M, times(N, M)))) [1]
gt(0, M) → False [1]
gt(NzN, 0) → u_4(is_NzNat(NzN)) [1]
u_4(True) → True [1]
is_NzNat(0) → False [1]
is_NzNat(s(N)) → True [1]
gt(s(N), s(M)) → gt(N, M) [1]
lt(N, M) → gt(M, N) [1]
d(0, N) → N [1]
d(s(N), s(M)) → d(N, M) [1]
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM) [1]
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM) [1]
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM)) [1]
quot(NzM, NzM) → u_01(is_NzNat(NzM)) [1]
u_01(True) → s(0) [1]
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N) [1]
u_21(True, NzM, N) → u_2(gt(NzM, N)) [1]
u_2(True) → 0 [1]
gcd(0, N) → 0 [1]
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM) [1]
u_02(True, NzM) → NzM [1]
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) [1]
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM) [1]
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM) [1]
p(s(N)) → N [1]
plus(N, 0) → N [1]
plus(s(N), s(M)) → s(s(plus(N, M))) [1]
times(N, 0) → 0 [1]
times(s(N), s(M)) → s(plus(N, plus(M, times(N, M)))) [1]
gt(0, M) → False [1]
gt(NzN, 0) → u_4(is_NzNat(NzN)) [1]
u_4(True) → True [1]
is_NzNat(0) → False [1]
is_NzNat(s(N)) → True [1]
gt(s(N), s(M)) → gt(N, M) [1]
lt(N, M) → gt(M, N) [1]
d(0, N) → N [1]
d(s(N), s(M)) → d(N, M) [1]
quot(N, NzM) → u_11(is_NzNat(NzM), N, NzM) [1]
u_11(True, N, NzM) → u_1(gt(N, NzM), N, NzM) [1]
u_1(True, N, NzM) → s(quot(d(N, NzM), NzM)) [1]
quot(NzM, NzM) → u_01(is_NzNat(NzM)) [1]
u_01(True) → s(0) [1]
quot(N, NzM) → u_21(is_NzNat(NzM), NzM, N) [1]
u_21(True, NzM, N) → u_2(gt(NzM, N)) [1]
u_2(True) → 0 [1]
gcd(0, N) → 0 [1]
gcd(NzM, NzM) → u_02(is_NzNat(NzM), NzM) [1]
u_02(True, NzM) → NzM [1]
gcd(NzN, NzM) → u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) [1]
u_31(True, True, NzN, NzM) → u_3(gt(NzN, NzM), NzN, NzM) [1]
u_3(True, NzN, NzM) → gcd(d(NzN, NzM), NzM) [1]
| p :: s:0 → s:0 s :: s:0 → s:0 plus :: s:0 → s:0 → s:0 0 :: s:0 times :: s:0 → s:0 → s:0 gt :: s:0 → s:0 → False:True False :: False:True u_4 :: False:True → False:True is_NzNat :: s:0 → False:True True :: False:True lt :: s:0 → s:0 → False:True d :: s:0 → s:0 → s:0 quot :: s:0 → s:0 → s:0 u_11 :: False:True → s:0 → s:0 → s:0 u_1 :: False:True → s:0 → s:0 → s:0 u_01 :: False:True → s:0 u_21 :: False:True → s:0 → s:0 → s:0 u_2 :: False:True → s:0 gcd :: s:0 → s:0 → s:0 u_02 :: False:True → s:0 → s:0 u_31 :: False:True → False:True → s:0 → s:0 → s:0 u_3 :: False:True → s:0 → s:0 → s:0 |
p(v0) → null_p [0]
plus(v0, v1) → null_plus [0]
times(v0, v1) → null_times [0]
u_4(v0) → null_u_4 [0]
d(v0, v1) → null_d [0]
u_11(v0, v1, v2) → null_u_11 [0]
u_1(v0, v1, v2) → null_u_1 [0]
u_01(v0) → null_u_01 [0]
u_21(v0, v1, v2) → null_u_21 [0]
u_2(v0) → null_u_2 [0]
u_02(v0, v1) → null_u_02 [0]
u_31(v0, v1, v2, v3) → null_u_31 [0]
u_3(v0, v1, v2) → null_u_3 [0]
gt(v0, v1) → null_gt [0]
is_NzNat(v0) → null_is_NzNat [0]
null_p, null_plus, null_times, null_u_4, null_d, null_u_11, null_u_1, null_u_01, null_u_21, null_u_2, null_u_02, null_u_31, null_u_3, null_gt, null_is_NzNat
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
False => 1
True => 2
null_p => 0
null_plus => 0
null_times => 0
null_u_4 => 0
null_d => 0
null_u_11 => 0
null_u_1 => 0
null_u_01 => 0
null_u_21 => 0
null_u_2 => 0
null_u_02 => 0
null_u_31 => 0
null_u_3 => 0
null_gt => 0
null_is_NzNat => 0
d(z, z') -{ 1 }→ N :|: z' = N, z = 0, N >= 0
d(z, z') -{ 1 }→ d(N, M) :|: z' = 1 + M, z = 1 + N, M >= 0, N >= 0
d(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
gcd(z, z') -{ 1 }→ u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM) :|: z = NzN, z' = NzM, NzM >= 0, NzN >= 0
gcd(z, z') -{ 1 }→ u_02(is_NzNat(NzM), NzM) :|: z = NzM, z' = NzM, NzM >= 0
gcd(z, z') -{ 1 }→ 0 :|: z' = N, z = 0, N >= 0
gt(z, z') -{ 1 }→ u_4(is_NzNat(NzN)) :|: z = NzN, NzN >= 0, z' = 0
gt(z, z') -{ 1 }→ gt(N, M) :|: z' = 1 + M, z = 1 + N, M >= 0, N >= 0
gt(z, z') -{ 1 }→ 1 :|: z' = M, z = 0, M >= 0
gt(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
is_NzNat(z) -{ 1 }→ 2 :|: z = 1 + N, N >= 0
is_NzNat(z) -{ 1 }→ 1 :|: z = 0
is_NzNat(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
lt(z, z') -{ 1 }→ gt(M, N) :|: z' = M, z = N, M >= 0, N >= 0
p(z) -{ 1 }→ N :|: z = 1 + N, N >= 0
p(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
plus(z, z') -{ 1 }→ N :|: z = N, z' = 0, N >= 0
plus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
plus(z, z') -{ 1 }→ 1 + (1 + plus(N, M)) :|: z' = 1 + M, z = 1 + N, M >= 0, N >= 0
quot(z, z') -{ 1 }→ u_21(is_NzNat(NzM), NzM, N) :|: z = N, z' = NzM, NzM >= 0, N >= 0
quot(z, z') -{ 1 }→ u_11(is_NzNat(NzM), N, NzM) :|: z = N, z' = NzM, NzM >= 0, N >= 0
quot(z, z') -{ 1 }→ u_01(is_NzNat(NzM)) :|: z = NzM, z' = NzM, NzM >= 0
times(z, z') -{ 1 }→ 0 :|: z = N, z' = 0, N >= 0
times(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
times(z, z') -{ 1 }→ 1 + plus(N, plus(M, times(N, M))) :|: z' = 1 + M, z = 1 + N, M >= 0, N >= 0
u_01(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
u_01(z) -{ 1 }→ 1 + 0 :|: z = 2
u_02(z, z') -{ 1 }→ NzM :|: z = 2, z' = NzM, NzM >= 0
u_02(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
u_1(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
u_1(z, z', z'') -{ 1 }→ 1 + quot(d(N, NzM), NzM) :|: z = 2, NzM >= 0, z' = N, z'' = NzM, N >= 0
u_11(z, z', z'') -{ 1 }→ u_1(gt(N, NzM), N, NzM) :|: z = 2, NzM >= 0, z' = N, z'' = NzM, N >= 0
u_11(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
u_2(z) -{ 1 }→ 0 :|: z = 2
u_2(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
u_21(z, z', z'') -{ 1 }→ u_2(gt(NzM, N)) :|: z = 2, z' = NzM, NzM >= 0, z'' = N, N >= 0
u_21(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
u_3(z, z', z'') -{ 1 }→ gcd(d(NzN, NzM), NzM) :|: z = 2, z' = NzN, NzM >= 0, z'' = NzM, NzN >= 0
u_3(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
u_31(z, z', z'', z1) -{ 1 }→ u_3(gt(NzN, NzM), NzN, NzM) :|: z = 2, z' = 2, z'' = NzN, NzM >= 0, z1 = NzM, NzN >= 0
u_31(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
u_4(z) -{ 1 }→ 2 :|: z = 2
u_4(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
| eq(start(V, V1, V2, V3),0,[p(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3),0,[plus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[times(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[gt(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[fun(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3),0,[fun1(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3),0,[lt(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[d(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[quot(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[fun2(V, V1, V2, Out)],[V >= 0,V1 >= 0,V2 >= 0]). eq(start(V, V1, V2, V3),0,[fun3(V, V1, V2, Out)],[V >= 0,V1 >= 0,V2 >= 0]). eq(start(V, V1, V2, V3),0,[fun4(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3),0,[fun5(V, V1, V2, Out)],[V >= 0,V1 >= 0,V2 >= 0]). eq(start(V, V1, V2, V3),0,[fun6(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3),0,[gcd(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[fun7(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3),0,[fun8(V, V1, V2, V3, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0]). eq(start(V, V1, V2, V3),0,[fun9(V, V1, V2, Out)],[V >= 0,V1 >= 0,V2 >= 0]). eq(p(V, Out),1,[],[Out = N1,V = 1 + N1,N1 >= 0]). eq(plus(V, V1, Out),1,[],[Out = N2,V = N2,V1 = 0,N2 >= 0]). eq(plus(V, V1, Out),1,[plus(N3, M1, Ret11)],[Out = 2 + Ret11,V1 = 1 + M1,V = 1 + N3,M1 >= 0,N3 >= 0]). eq(times(V, V1, Out),1,[],[Out = 0,V = N4,V1 = 0,N4 >= 0]). eq(times(V, V1, Out),1,[times(N5, M2, Ret111),plus(M2, Ret111, Ret112),plus(N5, Ret112, Ret1)],[Out = 1 + Ret1,V1 = 1 + M2,V = 1 + N5,M2 >= 0,N5 >= 0]). eq(gt(V, V1, Out),1,[],[Out = 1,V1 = M3,V = 0,M3 >= 0]). eq(gt(V, V1, Out),1,[fun1(NzN1, Ret0),fun(Ret0, Ret)],[Out = Ret,V = NzN1,NzN1 >= 0,V1 = 0]). eq(fun(V, Out),1,[],[Out = 2,V = 2]). eq(fun1(V, Out),1,[],[Out = 1,V = 0]). eq(fun1(V, Out),1,[],[Out = 2,V = 1 + N6,N6 >= 0]). eq(gt(V, V1, Out),1,[gt(N7, M4, Ret2)],[Out = Ret2,V1 = 1 + M4,V = 1 + N7,M4 >= 0,N7 >= 0]). eq(lt(V, V1, Out),1,[gt(M5, N8, Ret3)],[Out = Ret3,V1 = M5,V = N8,M5 >= 0,N8 >= 0]). eq(d(V, V1, Out),1,[],[Out = N9,V1 = N9,V = 0,N9 >= 0]). eq(d(V, V1, Out),1,[d(N10, M6, Ret4)],[Out = Ret4,V1 = 1 + M6,V = 1 + N10,M6 >= 0,N10 >= 0]). eq(quot(V, V1, Out),1,[fun1(NzM1, Ret01),fun2(Ret01, N11, NzM1, Ret5)],[Out = Ret5,V = N11,V1 = NzM1,NzM1 >= 0,N11 >= 0]). eq(fun2(V, V1, V2, Out),1,[gt(N12, NzM2, Ret02),fun3(Ret02, N12, NzM2, Ret6)],[Out = Ret6,V = 2,NzM2 >= 0,V1 = N12,V2 = NzM2,N12 >= 0]). eq(fun3(V, V1, V2, Out),1,[d(N13, NzM3, Ret10),quot(Ret10, NzM3, Ret12)],[Out = 1 + Ret12,V = 2,NzM3 >= 0,V1 = N13,V2 = NzM3,N13 >= 0]). eq(quot(V, V1, Out),1,[fun1(NzM4, Ret03),fun4(Ret03, Ret7)],[Out = Ret7,V = NzM4,V1 = NzM4,NzM4 >= 0]). eq(fun4(V, Out),1,[],[Out = 1,V = 2]). eq(quot(V, V1, Out),1,[fun1(NzM5, Ret04),fun5(Ret04, NzM5, N14, Ret8)],[Out = Ret8,V = N14,V1 = NzM5,NzM5 >= 0,N14 >= 0]). eq(fun5(V, V1, V2, Out),1,[gt(NzM6, N15, Ret05),fun6(Ret05, Ret9)],[Out = Ret9,V = 2,V1 = NzM6,NzM6 >= 0,V2 = N15,N15 >= 0]). eq(fun6(V, Out),1,[],[Out = 0,V = 2]). eq(gcd(V, V1, Out),1,[],[Out = 0,V1 = N16,V = 0,N16 >= 0]). eq(gcd(V, V1, Out),1,[fun1(NzM7, Ret06),fun7(Ret06, NzM7, Ret13)],[Out = Ret13,V = NzM7,V1 = NzM7,NzM7 >= 0]). eq(fun7(V, V1, Out),1,[],[Out = NzM8,V = 2,V1 = NzM8,NzM8 >= 0]). eq(gcd(V, V1, Out),1,[fun1(NzN2, Ret07),fun1(NzM9, Ret14),fun8(Ret07, Ret14, NzN2, NzM9, Ret15)],[Out = Ret15,V = NzN2,V1 = NzM9,NzM9 >= 0,NzN2 >= 0]). eq(fun8(V, V1, V2, V3, Out),1,[gt(NzN3, NzM10, Ret08),fun9(Ret08, NzN3, NzM10, Ret16)],[Out = Ret16,V = 2,V1 = 2,V2 = NzN3,NzM10 >= 0,V3 = NzM10,NzN3 >= 0]). eq(fun9(V, V1, V2, Out),1,[d(NzN4, NzM11, Ret09),gcd(Ret09, NzM11, Ret17)],[Out = Ret17,V = 2,V1 = NzN4,NzM11 >= 0,V2 = NzM11,NzN4 >= 0]). eq(p(V, Out),0,[],[Out = 0,V4 >= 0,V = V4]). eq(plus(V, V1, Out),0,[],[Out = 0,V5 >= 0,V6 >= 0,V = V5,V1 = V6]). eq(times(V, V1, Out),0,[],[Out = 0,V7 >= 0,V8 >= 0,V = V7,V1 = V8]). eq(fun(V, Out),0,[],[Out = 0,V9 >= 0,V = V9]). eq(d(V, V1, Out),0,[],[Out = 0,V10 >= 0,V11 >= 0,V = V10,V1 = V11]). eq(fun2(V, V1, V2, Out),0,[],[Out = 0,V12 >= 0,V2 = V13,V14 >= 0,V = V12,V1 = V14,V13 >= 0]). eq(fun3(V, V1, V2, Out),0,[],[Out = 0,V15 >= 0,V2 = V16,V17 >= 0,V = V15,V1 = V17,V16 >= 0]). eq(fun4(V, Out),0,[],[Out = 0,V18 >= 0,V = V18]). eq(fun5(V, V1, V2, Out),0,[],[Out = 0,V19 >= 0,V2 = V20,V21 >= 0,V = V19,V1 = V21,V20 >= 0]). eq(fun6(V, Out),0,[],[Out = 0,V22 >= 0,V = V22]). eq(fun7(V, V1, Out),0,[],[Out = 0,V23 >= 0,V24 >= 0,V = V23,V1 = V24]). eq(fun8(V, V1, V2, V3, Out),0,[],[Out = 0,V3 = V25,V26 >= 0,V2 = V27,V28 >= 0,V = V26,V1 = V28,V27 >= 0,V25 >= 0]). eq(fun9(V, V1, V2, Out),0,[],[Out = 0,V29 >= 0,V2 = V30,V31 >= 0,V = V29,V1 = V31,V30 >= 0]). eq(gt(V, V1, Out),0,[],[Out = 0,V32 >= 0,V33 >= 0,V = V32,V1 = V33]). eq(fun1(V, Out),0,[],[Out = 0,V34 >= 0,V = V34]). input_output_vars(p(V,Out),[V],[Out]). input_output_vars(plus(V,V1,Out),[V,V1],[Out]). input_output_vars(times(V,V1,Out),[V,V1],[Out]). input_output_vars(gt(V,V1,Out),[V,V1],[Out]). input_output_vars(fun(V,Out),[V],[Out]). input_output_vars(fun1(V,Out),[V],[Out]). input_output_vars(lt(V,V1,Out),[V,V1],[Out]). input_output_vars(d(V,V1,Out),[V,V1],[Out]). input_output_vars(quot(V,V1,Out),[V,V1],[Out]). input_output_vars(fun2(V,V1,V2,Out),[V,V1,V2],[Out]). input_output_vars(fun3(V,V1,V2,Out),[V,V1,V2],[Out]). input_output_vars(fun4(V,Out),[V],[Out]). input_output_vars(fun5(V,V1,V2,Out),[V,V1,V2],[Out]). input_output_vars(fun6(V,Out),[V],[Out]). input_output_vars(gcd(V,V1,Out),[V,V1],[Out]). input_output_vars(fun7(V,V1,Out),[V,V1],[Out]). input_output_vars(fun8(V,V1,V2,V3,Out),[V,V1,V2,V3],[Out]). input_output_vars(fun9(V,V1,V2,Out),[V,V1,V2],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [d/3]
1. non_recursive : [fun/2]
2. non_recursive : [fun1/2]
3. non_recursive : [fun4/2]
4. non_recursive : [fun6/2]
5. recursive : [gt/3]
6. non_recursive : [fun5/4]
7. recursive : [fun2/4,fun3/4,quot/3]
8. non_recursive : [fun7/3]
9. recursive : [fun8/5,fun9/4,gcd/3]
10. non_recursive : [lt/3]
11. non_recursive : [p/2]
12. recursive : [plus/3]
13. recursive [non_tail] : [times/3]
14. non_recursive : [start/4]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into d/3
1. SCC is partially evaluated into fun/2
2. SCC is partially evaluated into fun1/2
3. SCC is partially evaluated into fun4/2
4. SCC is partially evaluated into fun6/2
5. SCC is partially evaluated into gt/3
6. SCC is partially evaluated into fun5/4
7. SCC is partially evaluated into quot/3
8. SCC is partially evaluated into fun7/3
9. SCC is partially evaluated into gcd/3
10. SCC is completely evaluated into other SCCs
11. SCC is partially evaluated into p/2
12. SCC is partially evaluated into plus/3
13. SCC is partially evaluated into times/3
14. SCC is partially evaluated into start/4
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations d/3
* CE 29 is refined into CE [61]
* CE 27 is refined into CE [62]
* CE 28 is refined into CE [63]
### Cost equations --> "Loop" of d/3
* CEs [63] --> Loop 34
* CEs [61] --> Loop 35
* CEs [62] --> Loop 36
### Ranking functions of CR d(V,V1,Out)
* RF of phase [34]: [V,V1]
#### Partial ranking functions of CR d(V,V1,Out)
* Partial RF of phase [34]:
- RF of loop [34:1]:
V
V1
### Specialization of cost equations fun/2
* CE 49 is refined into CE [64]
* CE 48 is refined into CE [65]
### Cost equations --> "Loop" of fun/2
* CEs [64] --> Loop 37
* CEs [65] --> Loop 38
### Ranking functions of CR fun(V,Out)
#### Partial ranking functions of CR fun(V,Out)
### Specialization of cost equations fun1/2
* CE 51 is refined into CE [66]
* CE 52 is refined into CE [67]
* CE 50 is refined into CE [68]
### Cost equations --> "Loop" of fun1/2
* CEs [66] --> Loop 39
* CEs [67] --> Loop 40
* CEs [68] --> Loop 41
### Ranking functions of CR fun1(V,Out)
#### Partial ranking functions of CR fun1(V,Out)
### Specialization of cost equations fun4/2
* CE 54 is refined into CE [69]
* CE 53 is refined into CE [70]
### Cost equations --> "Loop" of fun4/2
* CEs [69] --> Loop 42
* CEs [70] --> Loop 43
### Ranking functions of CR fun4(V,Out)
#### Partial ranking functions of CR fun4(V,Out)
### Specialization of cost equations fun6/2
* CE 57 is refined into CE [71]
* CE 58 is refined into CE [72]
### Cost equations --> "Loop" of fun6/2
* CEs [71,72] --> Loop 44
### Ranking functions of CR fun6(V,Out)
#### Partial ranking functions of CR fun6(V,Out)
### Specialization of cost equations gt/3
* CE 26 is refined into CE [73]
* CE 24 is refined into CE [74,75,76,77]
* CE 23 is refined into CE [78]
* CE 25 is refined into CE [79]
### Cost equations --> "Loop" of gt/3
* CEs [79] --> Loop 45
* CEs [76] --> Loop 46
* CEs [78] --> Loop 47
* CEs [73,74,75,77] --> Loop 48
### Ranking functions of CR gt(V,V1,Out)
* RF of phase [45]: [V,V1]
#### Partial ranking functions of CR gt(V,V1,Out)
* Partial RF of phase [45]:
- RF of loop [45:1]:
V
V1
### Specialization of cost equations fun5/4
* CE 56 is refined into CE [80]
* CE 55 is refined into CE [81,82,83,84,85]
### Cost equations --> "Loop" of fun5/4
* CEs [82] --> Loop 49
* CEs [80,81,83,84,85] --> Loop 50
### Ranking functions of CR fun5(V,V1,V2,Out)
#### Partial ranking functions of CR fun5(V,V1,V2,Out)
### Specialization of cost equations quot/3
* CE 38 is refined into CE [86,87,88,89]
* CE 35 is refined into CE [90,91,92]
* CE 37 is refined into CE [93,94,95,96]
* CE 39 is refined into CE [97,98,99]
* CE 36 is refined into CE [100]
### Cost equations --> "Loop" of quot/3
* CEs [100] --> Loop 51
* CEs [88] --> Loop 52
* CEs [87,89] --> Loop 53
* CEs [93] --> Loop 54
* CEs [86,90,91,92,94,95,96,97,98,99] --> Loop 55
### Ranking functions of CR quot(V,V1,Out)
#### Partial ranking functions of CR quot(V,V1,Out)
### Specialization of cost equations fun7/3
* CE 60 is refined into CE [101]
* CE 59 is refined into CE [102]
### Cost equations --> "Loop" of fun7/3
* CEs [101] --> Loop 56
* CEs [102] --> Loop 57
### Ranking functions of CR fun7(V,V1,Out)
#### Partial ranking functions of CR fun7(V,V1,Out)
### Specialization of cost equations gcd/3
* CE 34 is refined into CE [103,104,105,106]
* CE 30 is refined into CE [107,108,109,110,111,112,113,114,115]
* CE 32 is refined into CE [116,117,118]
* CE 33 is refined into CE [119]
* CE 31 is refined into CE [120]
### Cost equations --> "Loop" of gcd/3
* CEs [120] --> Loop 58
* CEs [105] --> Loop 59
* CEs [104,106] --> Loop 60
* CEs [110,113] --> Loop 61
* CEs [103,107,108,109,111,112,114,115,116,117,118,119] --> Loop 62
### Ranking functions of CR gcd(V,V1,Out)
#### Partial ranking functions of CR gcd(V,V1,Out)
### Specialization of cost equations p/2
* CE 40 is refined into CE [121]
* CE 41 is refined into CE [122]
### Cost equations --> "Loop" of p/2
* CEs [121] --> Loop 63
* CEs [122] --> Loop 64
### Ranking functions of CR p(V,Out)
#### Partial ranking functions of CR p(V,Out)
### Specialization of cost equations plus/3
* CE 44 is refined into CE [123]
* CE 42 is refined into CE [124]
* CE 43 is refined into CE [125]
### Cost equations --> "Loop" of plus/3
* CEs [125] --> Loop 65
* CEs [123] --> Loop 66
* CEs [124] --> Loop 67
### Ranking functions of CR plus(V,V1,Out)
* RF of phase [65]: [V,V1]
#### Partial ranking functions of CR plus(V,V1,Out)
* Partial RF of phase [65]:
- RF of loop [65:1]:
V
V1
### Specialization of cost equations times/3
* CE 45 is refined into CE [126]
* CE 47 is refined into CE [127]
* CE 46 is refined into CE [128,129,130,131,132,133,134,135,136,137,138,139]
### Cost equations --> "Loop" of times/3
* CEs [138] --> Loop 68
* CEs [136] --> Loop 69
* CEs [139] --> Loop 70
* CEs [135] --> Loop 71
* CEs [131] --> Loop 72
* CEs [130] --> Loop 73
* CEs [129,133,134,137] --> Loop 74
* CEs [128,132] --> Loop 75
* CEs [126,127] --> Loop 76
### Ranking functions of CR times(V,V1,Out)
* RF of phase [68,69,70,71,74,75]: [V,V1]
#### Partial ranking functions of CR times(V,V1,Out)
* Partial RF of phase [68,69,70,71,74,75]:
- RF of loop [68:1,69:1,70:1,71:1]:
V1-1
- RF of loop [68:1,71:1]:
V-2
- RF of loop [69:1,70:1]:
V-1
- RF of loop [74:1,75:1]:
V
V1
### Specialization of cost equations start/4
* CE 2 is refined into CE [140]
* CE 3 is refined into CE [141,142,143]
* CE 4 is refined into CE [144,145,146,147,148]
* CE 5 is refined into CE [149,150,151,152,153,154]
* CE 6 is refined into CE [155,156,157]
* CE 7 is refined into CE [158,159,160,161,162]
* CE 8 is refined into CE [163,164,165,166,167,168]
* CE 9 is refined into CE [169,170]
* CE 10 is refined into CE [171,172,173,174]
* CE 11 is refined into CE [175,176,177]
* CE 12 is refined into CE [178,179,180,181,182]
* CE 13 is refined into CE [183,184]
* CE 14 is refined into CE [185,186,187]
* CE 15 is refined into CE [188,189,190,191,192]
* CE 16 is refined into CE [193,194,195]
* CE 17 is refined into CE [196,197,198,199]
* CE 18 is refined into CE [200,201]
* CE 19 is refined into CE [202]
* CE 20 is refined into CE [203]
* CE 21 is refined into CE [204,205,206]
* CE 22 is refined into CE [207,208]
### Cost equations --> "Loop" of start/4
* CEs [197,198,205,206] --> Loop 77
* CEs [171,179,188] --> Loop 78
* CEs [141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,183,200,207] --> Loop 79
* CEs [140,169,170,172,173,174,175,176,177,178,180,181,182,184,185,186,187,189,190,191,192,193,194,195,196,199,201,202,203,204,208] --> Loop 80
### Ranking functions of CR start(V,V1,V2,V3)
#### Partial ranking functions of CR start(V,V1,V2,V3)
Computing Bounds
=====================================
#### Cost of chains of d(V,V1,Out):
* Chain [[34],36]: 1*it(34)+1
Such that:it(34) =< V1-Out
with precondition: [Out+V=V1,V>=1,V1>=V]
* Chain [[34],35]: 1*it(34)+0
Such that:it(34) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [36]: 1
with precondition: [V=0,V1=Out,V1>=0]
* Chain [35]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of fun(V,Out):
* Chain [38]: 1
with precondition: [V=2,Out=2]
* Chain [37]: 0
with precondition: [Out=0,V>=0]
#### Cost of chains of fun1(V,Out):
* Chain [41]: 1
with precondition: [V=0,Out=1]
* Chain [40]: 0
with precondition: [Out=0,V>=0]
* Chain [39]: 1
with precondition: [Out=2,V>=1]
#### Cost of chains of fun4(V,Out):
* Chain [43]: 1
with precondition: [V=2,Out=1]
* Chain [42]: 0
with precondition: [Out=0,V>=0]
#### Cost of chains of fun6(V,Out):
* Chain [44]: 1
with precondition: [Out=0,V>=0]
#### Cost of chains of gt(V,V1,Out):
* Chain [[45],48]: 1*it(45)+2
Such that:it(45) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [[45],47]: 1*it(45)+1
Such that:it(45) =< V
with precondition: [Out=1,V>=1,V1>=V]
* Chain [[45],46]: 1*it(45)+3
Such that:it(45) =< V1
with precondition: [Out=2,V1>=1,V>=V1+1]
* Chain [48]: 2
with precondition: [Out=0,V>=0,V1>=0]
* Chain [47]: 1
with precondition: [V=0,Out=1,V1>=0]
* Chain [46]: 3
with precondition: [V1=0,Out=2,V>=1]
#### Cost of chains of fun5(V,V1,V2,Out):
* Chain [50]: 2*s(3)+1*s(4)+5
Such that:s(4) =< V1
aux(1) =< V2
s(3) =< aux(1)
with precondition: [Out=0,V>=0,V1>=0,V2>=0]
* Chain [49]: 5
with precondition: [V=2,V2=0,Out=0,V1>=1]
#### Cost of chains of quot(V,V1,Out):
* Chain [55]: 4*s(9)+7*s(10)+7
Such that:aux(2) =< V
aux(3) =< V1
s(10) =< aux(2)
s(9) =< aux(3)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [54]: 4
with precondition: [V=0,Out=0,V1>=1]
* Chain [53]: 2
with precondition: [Out=0,V1=V,V1>=0]
* Chain [52]: 3
with precondition: [Out=1,V1=V,V1>=1]
* Chain [51,55]: 6*s(9)+14
Such that:aux(5) =< V1
s(9) =< aux(5)
with precondition: [Out=1,V1>=1,V>=V1+1]
* Chain [51,54]: 2*s(21)+11
Such that:aux(4) =< V1
s(21) =< aux(4)
with precondition: [Out=1,V1>=1,V>=V1+1]
#### Cost of chains of fun7(V,V1,Out):
* Chain [57]: 1
with precondition: [V=2,V1=Out,V1>=0]
* Chain [56]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of gcd(V,V1,Out):
* Chain [62]: 2*s(31)+1*s(32)+7
Such that:s(32) =< V
aux(7) =< V1
s(31) =< aux(7)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [61]: 3
with precondition: [V1=0,Out=0,V>=0]
* Chain [60]: 2
with precondition: [Out=0,V1=V,V1>=0]
* Chain [59]: 3
with precondition: [V1=V,V1=Out,V1>=1]
* Chain [58,62]: 4*s(31)+15
Such that:aux(9) =< V1
s(31) =< aux(9)
with precondition: [Out=0,V1>=1,V>=V1+1]
#### Cost of chains of p(V,Out):
* Chain [64]: 0
with precondition: [Out=0,V>=0]
* Chain [63]: 1
with precondition: [V=Out+1,V>=1]
#### Cost of chains of plus(V,V1,Out):
* Chain [[65],67]: 1*it(65)+1
Such that:it(65) =< V1
with precondition: [V+V1=Out,V1>=1,V>=V1]
* Chain [[65],66]: 1*it(65)+0
Such that:it(65) =< Out/2
with precondition: [Out>=2,2*V>=Out,2*V1>=Out]
* Chain [67]: 1
with precondition: [V1=0,V=Out,V>=0]
* Chain [66]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of times(V,V1,Out):
* Chain [[68,69,70,71,74,75],76]: 13*it(68)+1*s(61)+1*s(62)+1*s(63)+3*s(64)+1*s(65)+1*s(67)+2*s(69)+1
Such that:aux(21) =< V
aux(19) =< V-V1
aux(25) =< V1
it(68) =< aux(21)
it(68) =< aux(25)
aux(17) =< aux(25)
aux(14) =< aux(21)
s(67) =< it(68)*aux(19)
s(63) =< it(68)*aux(25)
aux(13) =< it(68)*aux(21)
s(62) =< it(68)*aux(21)
s(70) =< it(68)*aux(17)
s(64) =< it(68)*aux(14)
s(65) =< it(68)*aux(17)
s(61) =< aux(13)* (1/2)
s(69) =< s(70)
with precondition: [V1>=1,Out>=1,2*V>=Out+1,V+2*V1>=Out+2]
* Chain [[68,69,70,71,74,75],73,76]: 13*it(68)+1*s(61)+1*s(62)+1*s(63)+3*s(64)+1*s(65)+1*s(67)+2*s(69)+1*s(71)+4
Such that:aux(21) =< V
aux(19) =< V-V1
aux(26) =< V1
s(71) =< aux(26)
it(68) =< aux(21)
it(68) =< aux(26)
aux(17) =< aux(26)
aux(14) =< aux(21)
s(67) =< it(68)*aux(19)
s(63) =< it(68)*aux(26)
aux(13) =< it(68)*aux(21)
s(62) =< it(68)*aux(21)
s(70) =< it(68)*aux(17)
s(64) =< it(68)*aux(14)
s(65) =< it(68)*aux(17)
s(61) =< aux(13)* (1/2)
s(69) =< s(70)
with precondition: [V1>=3,Out>=1,V>=V1,2*V>=Out+1,V+2*V1>=Out+2]
* Chain [[68,69,70,71,74,75],72,76]: 13*it(68)+1*s(61)+1*s(62)+1*s(63)+3*s(64)+1*s(65)+1*s(67)+2*s(69)+1*s(72)+3
Such that:aux(21) =< V
aux(19) =< V-V1
aux(27) =< V1
s(72) =< aux(27)
it(68) =< aux(21)
it(68) =< aux(27)
aux(17) =< aux(27)
aux(14) =< aux(21)
s(67) =< it(68)*aux(19)
s(63) =< it(68)*aux(27)
aux(13) =< it(68)*aux(21)
s(62) =< it(68)*aux(21)
s(70) =< it(68)*aux(17)
s(64) =< it(68)*aux(14)
s(65) =< it(68)*aux(17)
s(61) =< aux(13)* (1/2)
s(69) =< s(70)
with precondition: [V>=3,V1>=3,Out>=1,2*V>=Out+1,V+2*V1>=Out+2]
* Chain [76]: 1
with precondition: [Out=0,V>=0,V1>=0]
* Chain [73,76]: 1*s(71)+4
Such that:s(71) =< V1
with precondition: [V+V1=Out+1,Out>=V+1,2*V>=Out+1]
* Chain [72,76]: 1*s(72)+3
Such that:s(72) =< V1
with precondition: [Out>=3,2*V>=Out+1,2*V1>=Out+1]
#### Cost of chains of start(V,V1,V2,V3):
* Chain [80]: 29*s(106)+39*s(112)+3*s(115)+3*s(116)+3*s(118)+9*s(120)+3*s(121)+3*s(122)+6*s(123)+12*s(141)+2*s(156)+15
Such that:s(155) =< V2
aux(31) =< V
aux(32) =< V-V1
aux(33) =< V1
s(141) =< aux(31)
s(106) =< aux(33)
s(112) =< aux(31)
s(112) =< aux(33)
s(113) =< aux(33)
s(114) =< aux(31)
s(115) =< s(112)*aux(32)
s(116) =< s(112)*aux(33)
s(117) =< s(112)*aux(31)
s(118) =< s(112)*aux(31)
s(119) =< s(112)*s(113)
s(120) =< s(112)*s(114)
s(121) =< s(112)*s(113)
s(122) =< s(117)* (1/2)
s(123) =< s(119)
s(156) =< s(155)
with precondition: [V>=0]
* Chain [79]: 10*s(165)+49*s(171)+3*s(181)+8*s(182)+20
Such that:aux(42) =< -V1+V2
aux(43) =< V1
aux(44) =< V2
aux(45) =< V3
s(182) =< aux(42)
s(181) =< aux(43)
s(171) =< aux(44)
s(165) =< aux(45)
with precondition: [V=2]
* Chain [78]: 3
with precondition: [V1=0,V>=0]
* Chain [77]: 3
with precondition: [V=V1,V>=0]
Closed-form bounds of start(V,V1,V2,V3):
-------------------------------------
* Chain [80] with precondition: [V>=0]
- Upper bound: 51*V+15+27/2*V*V+nat(V1)*29+nat(V1)*12*V+nat(V2)*2+nat(V-V1)*3*V
- Complexity: n^2
* Chain [79] with precondition: [V=2]
- Upper bound: nat(V1)*3+20+nat(V2)*49+nat(V3)*10+nat(-V1+V2)*8
- Complexity: n
* Chain [78] with precondition: [V1=0,V>=0]
- Upper bound: 3
- Complexity: constant
* Chain [77] with precondition: [V=V1,V>=0]
- Upper bound: 3
- Complexity: constant
### Maximum cost of start(V,V1,V2,V3): nat(V1)*3+12+nat(V2)*2+max([nat(V2)*47+5+nat(V3)*10+nat(-V1+V2)*8,27/2*V*V+51*V+nat(V1)*26+nat(V1)*12*V+nat(V-V1)*3*V])+3
Asymptotic class: n^2
* Total analysis performed in 1165 ms.